cr{-}fails{-}before(${\it es}$; ${\it Sys}$; ${\it chain}$; $x$; $y$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$). (($y$ $\in$ ${\it chain}$($e$) $\in$ Id) \& ($\neg$($x$ $\in$ ${\it chain}$($e$) $\in$ Id)))